$\forall$$A$, $C$:Type, $B$:($A$$\rightarrow$Type), $x$:$a$:$A$ fp$\rightarrow$ $B$($a$), $f$:($a$:\{$a$:$A$$\mid$ ($a$ $\in$ fpf{-}domain($x$))\} $\rightarrow$$B$($a$)$\rightarrow$$C$).
\\[0ex]fpf{-}map($a$,$v$.$f$($a$,$v$);$x$) $\in$ ($C$ List)